import java.util.LinkedList;


public class Verificateur0 {
	
	public Verificateur0(){
		
	}
	
	public Invariant postCondition(Invariant inv, Affectation aff, 
									EnsembleVariable ev){
		int n = ev.size();
//		int index = ev.listeVariable.indexOf(aff.v);
		int index=0;
		while(!aff.v.nom.equals(ev.listeVariable.get(index).nom)){
			index++;
			if(index==n) System.out.println("AffectationToVariableUnknown");
		}		
		LinkedList<Inequalite> listIneNew = new LinkedList<Inequalite>();

		double aj=aff.expr.listExpr.get(index);
		//aj cas de inversible
		if(aj!=0){
			//pour chaque ine
			for(Inequalite ine : inv.invariant){
				LinkedList<Double> listtmp = new LinkedList<Double>();

				for (int i = 0; i < n; i++){
					if(i!=index){
						//calcule nouveau a(i) i!=j
						double aai = ine.expr.listExpr.get(i)-ine.expr.listExpr.get(index)/aj*aff.expr.listExpr.get(i);
						listtmp.add(i, aai);
					}
					else{
						//calcule nouveua a(j)
						double aaj = ine.expr.listExpr.get(index)/aj;
						listtmp.add(index, aaj);
					}
				}
				//calculte constant
				double dd = ine.expr.listExpr.get(n)-ine.expr.listExpr.get(index)/aj;//constant
				listtmp.add(n, dd);
//System.out.println("ajouter ok");
				Inequalite ineNew = new Inequalite(new Expression(listtmp));
				listIneNew.add(ineNew);
			}
			return new Invariant(listIneNew);
		}

		//aj cas de non-inversible
		else{
			LinkedList<Inequalite> listIneNewPos = new LinkedList<Inequalite>();
			LinkedList<Inequalite> listIneNewNeg = new LinkedList<Inequalite>();
			
			for(Inequalite ine : inv.invariant){
				double ajj=ine.expr.listExpr.get(index);
				//inequelite de type III
				if(ajj==0){
					 listIneNew.add(ine);
				}
				else{
					//inequalite de type I
					if (ajj>0){
						LinkedList<Double> dl= new LinkedList<Double>();
						//ajouter des coeffi
						for(int i = 0; i<n ; i++){
							if(i!=index){
								dl.add(i, (-1)*ine.expr.listExpr.get(i)/ajj);
							}
							else{
								dl.add(index,0.0);
							}
						}
						//ajouter constant
						dl.add(n, (-1)*ine.expr.listExpr.get(n)/ajj);
						listIneNewPos.add(new Inequalite(new Expression(dl)));
					}
					//inequelite de type II
					if (ajj<0){
						LinkedList<Double> dl= new LinkedList<Double>();
						//ajouter des coeffi
						for(int i = 0; i<n ; i++){
							if(i!=index){
								dl.add(i, (-1)*ine.expr.listExpr.get(i)/ajj);
							}
							else{
								dl.add(index,0.0);
							}
						}
						//ajouter constant
						dl.add(n, (-1)*ine.expr.listExpr.get(n)/ajj);
						listIneNewNeg.add(new Inequalite(new Expression(dl)));
					}
				} 
			}
			
			for (Inequalite inePos:listIneNewPos){
				for (Inequalite ineNeg:listIneNewNeg){
					LinkedList<Double> dll = new LinkedList<Double>();
					for(int i = 0; i< n+1; i++){
						double tmp = ineNeg.expr.listExpr.get(i)-inePos.expr.listExpr.get(i);
						dll.add(i, tmp);
					}
					Inequalite ineNew = new Inequalite(new Expression(dll));
					listIneNew.add(ineNew);
				}
			}
			return new Invariant(listIneNew);
		}
	}
	
	
	
	
	public static void main(String[] args) {
    	// le main prend le fichier t1.txt et affiche les variable
		//pour l instant, on suppose qu' il n'y a pas de "space"(ascii=32) in .txt.
	    	EnsembleVariable ens = new EnsembleVariable("t1.txt");
	    	
	    	for (int i = 0; i < ens.size(); i++)
	    		System.out.print(ens.getVariable(i).nom+",");
	    	System.out.println(ens.size() + " Variables");
//	    	Expression ex = new Expression("+1+23*i-4*j0+6000*k",ens);ex.publish(ens);System.out.println();
//	    	Inequalite ine = new Inequalite("+1+23*i-4*j0+6000*k<=0",ens);ine.pulish(ens);System.out.println();
//	    	Invariant inv = new Invariant("{+0+1*i+1*j0+1*k>=0,+0+1*i+2*j0+3*k<=0}",ens);inv.publish(ens);
//	    	Affectation aff = new Affectation("[i=+1+23*i-4*j0+6000*k]",ens);aff.publish(ens);System.out.println();
	   /*	
	    	String testStr1 = "{+0+1*i+1*j0+1*k>=0,+1+1*i+2*j0+3*k<=0}\n" +
	    			"[i=+2+23*i-4*j0+600*k]\n" +
	    			"{+3+23*i-4*j0+60*k<=0,+4+23*i-4*j0+6*k>=0}\n" +
	    			"[i=+5+23*i-4*j0+600*k]\n" +
	    			"{+6+23*i-4*j0+6*k>=0}\n" +
	    			"@";
	    */
	   // 	System.out.println(testStr1.length());
	  //  	System.out.println("\n ".length()); //=2
	    //	Block blc = new Block(testStr1,ens);blc.publish(ens);
//	    /*	
	    	Verificateur0 verif = new Verificateur0();
	    	Invariant inv0 = new Invariant();
	    	Invariant invv = new Invariant("{+1+1*i+1*j0+1*k>=0,+0+1*i+2*j0+1*k<=0,+0+1*i+0*j0+1*k>=0}",ens);//tester typeIII:typeI=1,typeII=1,typeIII=1
//	    	Invariant invv = new Invariant("{+1+1*i+1*j0+1*k>=0,+0+1*i+2*j0+1*k<=0}",ens);//tester typeI=1,typeII=1,typeIII=0
//	    	Invariant invv = new Invariant("{+1+1*i+1*j0+1*k>=0,+0+1*i+2*j0+1*k>=0,+0+1*i+0*j0+1*k>=0}",ens);//tester typeI=2,typeII=0
	    	Affectation afff = new Affectation("[j0=+1+0*i+2*j0+0*k]",ens);//affectation inversible
//	    	Affectation afff = new Affectation("[j0=+1+0*i+0*j0+0*k]",ens);//affectation non-inversible
	    	inv0 = verif.postCondition(invv, afff, ens);
	    	inv0.publish(ens);
//	     */
	}
}
